$\forall$$a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:Top, $x$:Id, $t$:Type, $v$:$t$.
\\[0ex]${\it ds}$ $\parallel$ $x$ : $t$
\\[0ex]$\Rightarrow$ ((with ds: ${\it ds}$ action $a$:$T$ precondition $a$(v) is $P$ s v) $\Vert\!+$ $x$ : $t$ initially $x$ = $v$)